package esctest;

public class MaxTest {
	/*@
	  @ public normal_behavior
	  @ ensures (x >= y) ==> \result == x;
	  @ ensures (y >= x) ==> \result == y; 
	  @*/
	public static int max(int x, int y) {
		int ret = y;
//		int ret = 0;
		if (x > y) {
			ret = x;
//		} else if (y > x) {
//			ret = y;
		}
		return ret;
	}
}
